$\forall$$M$:MsgA, $k$:Knd, $x$:Id. $M$.aframe($k$ affects $x$) $\in$ Prop